Inference at * 1 1 
Iof proof for Lemma last-not-before:

.....antecedent..... NILNIL

1. T : Type
2. L : T List
3. (null(L))
4. no_repeats(T;L)
5. x : T
6. last(L) before x  L
7. x, y:T. x before y  L  ((x = y))
8. (last(L) = x)
  (x  L) 

latex

 by ((FLemma `l_before_member` [-3]) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	x:A. B(x), P  Q, x:AB(x), (x  l)
Lemmas	l before member